Model checking is a formal method for proving that a finite-state model satisfies a user-specified property. As a result of the development of symbolic state space traversal algorithms based on Binary Decision Diagrams (BDDs) and Boolean Satisfiability Solvers (SAT), model checking has become widely recognized as an effective technique for hardware verification. Its utility is not limited to hardware however therefore model checking is being used for software verification as well—especially for transaction-level system designs (in SystemC, for example) and in embedded software (e.g., C/C++).
As is known by those skilled in the art, complexities associated with model checking methods depend upon the size of the state space being modeled which is generally exponential in terms of the number of state variables (or memory elements) of the particular model employed. This exponential dependence may easily cause what is known in the art as memory “blow up”—a major hurdle to be overcome in applying model checking to relatively large systems.
One methodology which partially addressed the exponential dependence and resulting memory explosion is through the use of BDDs. BDD based symbolic model checking was first described by K. McMillan in a book entitled “Symbolic Model Checking”, published by Kluwer in 1993. As described by F. Ivancic, I. Shlyakhter, A. Gupta, M. K. Ganai, V. Kahlon, C. Wang and Z. Yang in a paper entitled “Model Checking C Program Using F-Soft”, which appeared in Proceedings of IEEE International Conference on Computer Design, 2005, BDD based symbolic model checking traverses the state space symbolically by employing symbolic graph algorithms that represent sets of states in Boolean functions. Consequently, their complexity depends upon the size of the BDD representations instead of the number of states. And while symbolic model checking can effectively manage much larger models, it too is subject to the blow-up problem described previously.
As a result, formal verification researchers have searched for heuristics that avoid this BDD blow up. One such approach involves efficient algorithms for conducting image computation—a fundamental computation in symbolic model checking—which has been extensively studied and characterized for hardware models, in particular. (See, e.g., O. Coudert, et al., “Verification of Sequential Machines Based on Symbolic Execution”; in Automatic Verification Methods for Finite State Systems, J. Sifakis, ed., pp. 365-373, Springer-Verlag, 1989).
Software models however, exhibit certain unique characteristics that make them significantly more difficult for the application of existing model checkers. First, the number of state variables (or memory elements) in a software model is typically much larger than that found in a hardware model. Additionally, and as compared with hardware models, software models usually have much deeper sequential depths. As such, without wide counters, an arbitrary state of a hardware model can often be reached within only a few clock cycles. For most software models however, the number of steps required to reach a particular state may be orders of magnitude larger. Consequently, conventional BDD based model checking algorithms do not work particularly well on software models. (See, e.g., S. Edwards et al., “Using A Hardware Model Checker To Verify Software”, Proceedings of the 4th International Converence on ASIC (ASICON '01), IEEE, October 2001.)
As a result, new approaches of model checking more directly applicable to software models would represent a significant advance in the art. Such an approach is the subject of the instant invention.